Inference at * 1 0 4 1 
Iof proof for Lemma eq int cases test:

.....assertion..... NILNIL

1. A : Type
2. x : A
3. y : A
4. P : A
5. i : 
6. j : 
7. P(if (i = j) then x else y fi )
8.   Type
9. (i = j)  
10. bb:. ((i = j) = bb)  Type
  bb:. ((i = j) = bb) 

latex

 by (\p.At (get_term_arg `UA` p) 
 by ((DTerm (get_term_arg `e` p) 0) p) 

latex

 1: .....wf..... NILNIL

 1:   (i = j)  
 2: 

 2:   (i = j) = (i = j)
 3: .....wf..... NILNIL

 3: 11. bb : 
 3:   ((i = j) = bb)  Type
 .

Definitions

s = t, x:A. B(x), , (i = j), if b then t else f fi , f(a), , , x:AB(x), Type, x:A  B(x), x:A. B(x), t  T